|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
|
|
|
Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Pavela, Ondřej ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Looper is a static complexity analysis tool for inference of tight upper bounds on the exe- cution cost of programs. It is based on the previously existing Loopus tool which used abstract program model of difference constraints (inequalities of the form + ), which allows for natural abstraction of common loop counter updates = + + and = + 0. Looper was initially proposed and implemented in author’s bachelor’s thesis as a checker for the Meta Infer framework but the tool failed to meet the expectations when tested on real-world code. This master’s thesis proposes a new improved version of Looper that aims at solving the main limitations of the original tool, namely through introduction of interprocedural analysis. Additionally, various extensions target- ing improved precision of the intraprocedural analysis, such as new abstraction algorithm, handling of compound loop conditions and more, were implemented. Moreover, logging, issue reporting and collection of results has been significantly improved. Finally, through extensive experiments with the new Looper version, the ability to analyze real-world code in a more general, scalable and precise way was shown.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
|
|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
host ::
RSS.